Skip to content

Add Windows MSVC test support: rng_fail, alloc, wycheproof#1738

Open
willieyz wants to merge 3 commits into
mainfrom
win-sup-rng-fail
Open

Add Windows MSVC test support: rng_fail, alloc, wycheproof#1738
willieyz wants to merge 3 commits into
mainfrom
win-sup-rng-fail

Conversation

@willieyz

@willieyz willieyz commented Jun 8, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

mlkem-native already runs tests on Windows via Mingw-w64, but the MSVC/nmake build only covers the functional tests. This PR closes the remaining gap by adding the following tests to Makefile.Microsoft_nmake, against the portable C backend:

  • rng_fail: link rules added.
  • alloc: added test/src/test_alloc.c and test/configs/test_alloc_config.h, referencing the Linux Makefile. Needs to rebuild the .obj files since it uses a different config from the default functional test. A new ALLOC_CFLAGS macro keeps the build rules short.
  • wycheproof: test obj building rules and link rules added.

Unit tests are intentionally omitted from this PR and can be added later once native backend support becomes available on Windows.

@oqs-bot

oqs-bot commented Jun 8, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-512)

Full Results (191 proofs)
Proof Status Current Previous Change
**TOTAL** ✅ 1688s 1531s +10.3%
mlk_indcpa_enc ✅ 257s 255s +1%
mlk_indcpa_keypair_derand ✅ 227s 213s +7%
mlk_poly_rej_uniform ✅ 162s 135s +20%
mlk_rej_uniform_c ✅ 138s 112s +23%
rej_uniform_native_x86_64 ✅ 62s 55s +13%
mlk_polyvec_basemul_acc_montgomery_cached_c ✅ 59s 51s +16%
poly_ntt_native ✅ 43s 33s +30%
mlk_poly_reduce_native ✅ 41s 32s +28%
rej_uniform_native_aarch64 ✅ 39s 33s +18%
mlk_ntt_layer ✅ 38s 27s +41%
mlk_keccak_squeezeblocks_x4 ✅ 28s 26s +8%
mlk_fqmul ✅ 18s 15s +20%
keccakf1600x4_permute_native_x4 ✅ 17s 17s +0%
mlk_poly_decompress_d10_native ✅ 17s 12s +42%
mlk_indcpa_dec ✅ 16s 13s +23%
mlk_poly_decompress_d4_native ✅ 14s 13s +8%
mlk_poly_frommsg ✅ 13s 11s +18%
mlk_polyvec_add ✅ 10s 11s -9%
mlk_poly_frombytes_native ✅ 9s 9s +0%
mlk_poly_ntt ✅ 9s 6s +50%
mlk_keccak_squeeze_once ✅ 8s 8s +0%
polyvec_basemul_acc_montgomery_cached_native ✅ 8s 8s +0%
mlk_keccak_squeezeblocks ✅ 7s 8s -12%
mlk_ntt_butterfly_block ✅ 7s 8s -12%
mlk_poly_add ✅ 7s 4s +75%
mlk_poly_rej_uniform_x4 ✅ 7s 5s +40%
mlk_poly_sub ✅ 7s 8s -12%
mlk_invntt_layer ✅ 6s 5s +20%
mlk_keccakf1600_permute_c ✅ 6s 5s +20%
poly_decompress_d10_native_x86_64 ✅ 6s 3s +100%
poly_frombytes_native_x86_64 ✅ 6s 6s +0%
kem_dec ✅ 5s 3s +67%
mlk_keccak_absorb_once ✅ 5s 3s +67%
mlk_keccak_absorb_once_x4 ✅ 5s 6s -17%
mlk_poly_decompress_d5_native ✅ 5s 2s +150%
mlk_poly_frombytes_c ✅ 5s 5s +0%
mlk_poly_getnoise_eta1_4x_native ✅ 5s 4s +25%
mlk_polyvec_invntt_tomont ✅ 5s 4s +25%
poly_decompress_d4_native_x86_64 ✅ 5s 5s +0%
kem_check_sk ✅ 4s 2s +100%
kem_enc_derand ✅ 4s 3s +33%
mlk_keccakf1600_xor_bytes ✅ 4s 2s +100%
mlk_poly_cbd_eta2 ✅ 4s 2s +100%
mlk_poly_compress_d4_c ✅ 4s 5s -20%
mlk_poly_compress_dv ✅ 4s 1s +300%
mlk_poly_decompress_d11 ✅ 4s 2s +100%
mlk_poly_decompress_d4 ✅ 4s 2s +100%
mlk_poly_decompress_d4_c ✅ 4s 4s +0%
mlk_poly_decompress_d5 ✅ 4s 2s +100%
mlk_poly_invntt_tomont_c ✅ 4s 3s +33%
mlk_poly_reduce ✅ 4s 2s +100%
mlk_polyvec_basemul_acc_montgomery_cached ✅ 4s 2s +100%
mlk_polyvec_permute_bitrev_to_custom_native ✅ 4s 1s +300%
mlk_shake256x4 ✅ 4s 5s -20%
poly_compress_d10_native_x86_64 ✅ 4s 5s -20%
poly_tomont_native_x86_64 ✅ 4s 3s +33%
intt_native_aarch64 ✅ 3s 3s +0%
intt_native_x86_64 ✅ 3s 4s -25%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid ✅ 3s 2s +50%
kem_keypair_derand ✅ 3s 5s -40%
mlk_check_pct ✅ 3s 1s +200%
mlk_ct_cmov_zero ✅ 3s 2s +50%
mlk_ct_get_optblocker_u32 ✅ 3s 1s +200%
mlk_keccakf1600_xor_bytes (big endian) ✅ 3s 3s +0%
mlk_keccakf1600x4_permute ✅ 3s 1s +200%
mlk_keccakf1600x4_xor_bytes_c ✅ 3s 2s +50%
mlk_poly_cbd_eta1 ✅ 3s 2s +50%
mlk_poly_compress_d10_c ✅ 3s 5s -40%
mlk_poly_compress_d4 ✅ 3s 2s +50%
mlk_poly_compress_d4_native ✅ 3s 5s -40%
mlk_poly_compress_d5_c ✅ 3s 3s +0%
mlk_poly_compress_du ✅ 3s 3s +0%
mlk_poly_decompress_d11_c ✅ 3s 1s +200%
mlk_poly_decompress_dv ✅ 3s 4s -25%
mlk_poly_getnoise_eta1_4x ✅ 3s 2s +50%
mlk_poly_getnoise_eta2 ✅ 3s 3s +0%
mlk_poly_invntt_tomont ✅ 3s 2s +50%
mlk_poly_mulcache_compute ✅ 3s 2s +50%
mlk_poly_mulcache_compute_c ✅ 3s 3s +0%
mlk_poly_tomont_c ✅ 3s 3s +0%
mlk_poly_tomsg ✅ 3s 2s +50%
mlk_polyvec_decompress_du ✅ 3s 2s +50%
mlk_polyvec_frombytes ✅ 3s 2s +50%
mlk_polyvec_ntt ✅ 3s 1s +200%
mlk_polyvec_permute_bitrev_to_custom ✅ 3s 1s +200%
mlk_polyvec_tobytes ✅ 3s 3s +0%
mlk_scalar_compress_d10 ✅ 3s 2s +50%
mlk_scalar_decompress_d11 ✅ 3s 4s -25%
mlk_scalar_decompress_d5 ✅ 3s 4s -25%
mlk_scalar_signed_to_unsigned_q ✅ 3s 4s -25%
mlk_shake128_absorb_once ✅ 3s 3s +0%
mlk_value_barrier_u32 ✅ 3s 2s +50%
ntt_native_x86_64 ✅ 3s 1s +200%
nttunpack_native_x86_64 ✅ 3s 3s +0%
poly_compress_d4_native_x86_64 ✅ 3s 2s +50%
poly_decompress_d11_native_x86_64 ✅ 3s 3s +0%
poly_invntt_tomont_native ✅ 3s 1s +200%
poly_tomont_native_aarch64 ✅ 3s 1s +200%
polyvec_basemul_acc_montgomery_cached_k2_native_aarch64 ✅ 3s 4s -25%
rej_uniform_native ✅ 3s 2s +50%
sys_check_capability ✅ 3s 1s +200%
keccak_f1600_x1_native_aarch64 ✅ 2s 2s +0%
keccak_f1600_x1_native_aarch64_v84a ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid ✅ 2s 3s -33%
keccakf1600_permute_native ✅ 2s 1s +100%
keccakf1600x4_xor_bytes_native ✅ 2s 2s +0%
kem_enc ✅ 2s 2s +0%
kem_keypair ✅ 2s 3s -33%
mlk_ct_cmask_neg_i16 ✅ 2s 1s +100%
mlk_ct_cmask_nonzero_u16 ✅ 2s 4s -50%
mlk_ct_cmask_nonzero_u8 ✅ 2s 5s -60%
mlk_ct_get_optblocker_i32 ✅ 2s 2s +0%
mlk_ct_get_optblocker_u8 ✅ 2s 2s +0%
mlk_ct_sel_int16 ✅ 2s 1s +100%
mlk_ct_sel_uint8 ✅ 2s 2s +0%
mlk_enc_getnoise_eta1_eta2 ✅ 2s 2s +0%
mlk_gen_matrix_serial ✅ 2s 2s +0%
mlk_keccakf1600_extract_bytes ✅ 2s 2s +0%
mlk_keccakf1600_extract_bytes (big endian) ✅ 2s 1s +100%
mlk_keccakf1600_permute ✅ 2s 1s +100%
mlk_keccakf1600x4_extract_bytes_c ✅ 2s 1s +100%
mlk_keccakf1600x4_xor_bytes ✅ 2s 1s +100%
mlk_montgomery_reduce ✅ 2s 1s +100%
mlk_poly_compress_d10 ✅ 2s 5s -60%
mlk_poly_compress_d11 ✅ 2s 1s +100%
mlk_poly_compress_d11_native ✅ 2s 2s +0%
mlk_poly_compress_d5 ✅ 2s 1s +100%
mlk_poly_decompress_d10 ✅ 2s 5s -60%
mlk_poly_decompress_d10_c ✅ 2s 2s +0%
mlk_poly_decompress_d11_native ✅ 2s 2s +0%
mlk_poly_decompress_d5_c ✅ 2s 1s +100%
mlk_poly_getnoise_eta1122_4x ✅ 2s 1s +100%
mlk_poly_mulcache_compute_native ✅ 2s 2s +0%
mlk_poly_ntt_c ✅ 2s 2s +0%
mlk_poly_reduce_c ✅ 2s 1s +100%
mlk_poly_tobytes ✅ 2s 3s -33%
mlk_poly_tobytes_c ✅ 2s 2s +0%
mlk_poly_tobytes_native ✅ 2s 3s -33%
mlk_poly_tomont ✅ 2s 2s +0%
mlk_polymat_permute_bitrev_to_custom ✅ 2s 2s +0%
mlk_polyvec_compress_du ✅ 2s 3s -33%
mlk_polyvec_reduce ✅ 2s 1s +100%
mlk_polyvec_tomont ✅ 2s 3s -33%
mlk_rej_uniform ✅ 2s 1s +100%
mlk_scalar_compress_d4 ✅ 2s 2s +0%
mlk_scalar_decompress_d10 ✅ 2s 3s -33%
mlk_scalar_decompress_d4 ✅ 2s 4s -50%
mlk_sha3_256 ✅ 2s 2s +0%
mlk_sha3_512 ✅ 2s 1s +100%
mlk_shake128x4_absorb_once ✅ 2s 3s -33%
mlk_shake128x4_squeezeblocks ✅ 2s 4s -50%
mlk_value_barrier_i32 ✅ 2s 1s +100%
mlk_value_barrier_u8 ✅ 2s 2s +0%
ntt_native_aarch64 ✅ 2s 1s +100%
poly_compress_d5_native_x86_64 ✅ 2s 2s +0%
poly_decompress_d5_native_x86_64 ✅ 2s 2s +0%
poly_getnoise_eta1122_4x_native ✅ 2s 2s +0%
poly_mulcache_compute_native_x86_64 ✅ 2s 2s +0%
poly_reduce_native_aarch64 ✅ 2s 2s +0%
poly_reduce_native_x86_64 ✅ 2s 4s -50%
poly_tobytes_native_aarch64 ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_k2_native_x86_64 ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_k3_native_x86_64 ✅ 2s 3s -33%
polyvec_basemul_acc_montgomery_cached_k4_native_aarch64 ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v84a ✅ 1s 2s -50%
keccak_f1600_x4_native_avx2 ✅ 1s 1s +0%
keccakf1600x4_extract_bytes_native ✅ 1s 3s -67%
kem_check_pk ✅ 1s 2s -50%
mlk_barrett_reduce ✅ 1s 3s -67%
mlk_ct_memcmp ✅ 1s 1s +0%
mlk_gen_matrix ✅ 1s 3s -67%
mlk_keccakf1600x4_extract_bytes ✅ 1s 3s -67%
mlk_keypair_getnoise_eta1 ✅ 1s 2s -50%
mlk_matvec_mul ✅ 1s 1s +0%
mlk_poly_compress_d10_native ✅ 1s 2s -50%
mlk_poly_compress_d11_c ✅ 1s 2s -50%
mlk_poly_compress_d5_native ✅ 1s 2s -50%
mlk_poly_decompress_du ✅ 1s 2s -50%
mlk_poly_frombytes ✅ 1s 2s -50%
mlk_poly_tomont_native ✅ 1s 3s -67%
mlk_polyvec_mulcache_compute ✅ 1s 2s -50%
mlk_scalar_compress_d1 ✅ 1s 4s -75%
mlk_scalar_compress_d11 ✅ 1s 1s +0%
mlk_scalar_compress_d5 ✅ 1s 4s -75%
mlk_shake128_squeezeblocks ✅ 1s 2s -50%
mlk_shake256 ✅ 1s 2s -50%
poly_compress_d11_native_x86_64 ✅ 1s 3s -67%
poly_mulcache_compute_native_aarch64 ✅ 1s 2s -50%
poly_tobytes_native_x86_64 ✅ 1s 2s -50%
polyvec_basemul_acc_montgomery_cached_k3_native_aarch64 ✅ 1s 2s -50%
polyvec_basemul_acc_montgomery_cached_k4_native_x86_64 ✅ 1s 2s -50%

@oqs-bot

oqs-bot commented Jun 8, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-1024)

Full Results (191 proofs)
Proof Status Current Previous Change
**TOTAL** ✅ 1761s 1673s +5.3%
mlk_indcpa_enc ✅ 384s 381s +1%
mlk_indcpa_keypair_derand ✅ 171s 160s +7%
mlk_poly_rej_uniform ✅ 144s 133s +8%
mlk_rej_uniform_c ✅ 136s 112s +21%
mlk_polyvec_basemul_acc_montgomery_cached_c ✅ 71s 65s +9%
rej_uniform_native_x86_64 ✅ 58s 58s +0%
poly_ntt_native ✅ 39s 35s +11%
mlk_ntt_layer ✅ 37s 28s +32%
rej_uniform_native_aarch64 ✅ 37s 34s +9%
mlk_poly_reduce_native ✅ 35s 34s +3%
polyvec_basemul_acc_montgomery_cached_native ✅ 26s 28s -7%
mlk_keccak_squeezeblocks_x4 ✅ 25s 26s -4%
mlk_polyvec_add ✅ 19s 17s +12%
mlk_fqmul ✅ 17s 17s +0%
keccakf1600x4_permute_native_x4 ✅ 15s 15s +0%
mlk_poly_decompress_d5_native ✅ 15s 13s +15%
mlk_poly_decompress_d11_native ✅ 14s 13s +8%
mlk_indcpa_dec ✅ 12s 11s +9%
mlk_polyvec_ntt ✅ 12s 9s +33%
mlk_poly_frombytes_native ✅ 10s 9s +11%
mlk_poly_frommsg ✅ 9s 8s +12%
mlk_keccak_squeeze_once ✅ 8s 7s +14%
mlk_keccak_squeezeblocks ✅ 8s 9s -11%
mlk_keccak_absorb_once_x4 ✅ 7s 7s +0%
mlk_ntt_butterfly_block ✅ 7s 6s +17%
mlk_poly_ntt ✅ 7s 6s +17%
mlk_gen_matrix_serial ✅ 6s 7s -14%
mlk_invntt_layer ✅ 6s 9s -33%
mlk_keccakf1600_permute_c ✅ 6s 4s +50%
mlk_poly_add ✅ 6s 6s +0%
mlk_poly_rej_uniform_x4 ✅ 6s 6s +0%
mlk_poly_sub ✅ 6s 7s -14%
mlk_polymat_permute_bitrev_to_custom ✅ 6s 4s +50%
kem_dec ✅ 5s 4s +25%
mlk_gen_matrix ✅ 5s 2s +150%
mlk_montgomery_reduce ✅ 5s 1s +400%
mlk_poly_getnoise_eta1_4x ✅ 5s 3s +67%
mlk_shake256x4 ✅ 5s 3s +67%
polyvec_basemul_acc_montgomery_cached_k4_native_x86_64 ✅ 5s 2s +150%
keccakf1600_permute_native ✅ 4s 2s +100%
mlk_keccakf1600_xor_bytes (big endian) ✅ 4s 2s +100%
mlk_keypair_getnoise_eta1 ✅ 4s 3s +33%
mlk_poly_cbd_eta1 ✅ 4s 3s +33%
mlk_poly_compress_d10 ✅ 4s 2s +100%
mlk_poly_compress_d10_c ✅ 4s 2s +100%
mlk_poly_compress_d11_c ✅ 4s 4s +0%
mlk_poly_decompress_d11_c ✅ 4s 2s +100%
mlk_poly_decompress_d4_c ✅ 4s 3s +33%
mlk_poly_frombytes_c ✅ 4s 6s -33%
mlk_scalar_compress_d1 ✅ 4s 2s +100%
mlk_shake128_squeezeblocks ✅ 4s 1s +300%
poly_compress_d10_native_x86_64 ✅ 4s 4s +0%
poly_decompress_d11_native_x86_64 ✅ 4s 4s +0%
poly_mulcache_compute_native_x86_64 ✅ 4s 4s +0%
poly_tomont_native_x86_64 ✅ 4s 2s +100%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid ✅ 3s 2s +50%
keccakf1600x4_extract_bytes_native ✅ 3s 2s +50%
keccakf1600x4_xor_bytes_native ✅ 3s 1s +200%
kem_check_pk ✅ 3s 3s +0%
kem_check_sk ✅ 3s 1s +200%
kem_enc_derand ✅ 3s 3s +0%
mlk_check_pct ✅ 3s 3s +0%
mlk_ct_cmask_nonzero_u16 ✅ 3s 1s +200%
mlk_ct_cmask_nonzero_u8 ✅ 3s 4s -25%
mlk_ct_get_optblocker_u32 ✅ 3s 1s +200%
mlk_ct_sel_int16 ✅ 3s 1s +200%
mlk_enc_getnoise_eta1_eta2 ✅ 3s 1s +200%
mlk_keccak_absorb_once ✅ 3s 3s +0%
mlk_keccakf1600_xor_bytes ✅ 3s 2s +50%
mlk_keccakf1600x4_extract_bytes ✅ 3s 4s -25%
mlk_poly_cbd_eta2 ✅ 3s 2s +50%
mlk_poly_compress_d4 ✅ 3s 2s +50%
mlk_poly_compress_du ✅ 3s 3s +0%
mlk_poly_compress_dv ✅ 3s 3s +0%
mlk_poly_decompress_d10 ✅ 3s 2s +50%
mlk_poly_decompress_d4_native ✅ 3s 2s +50%
mlk_poly_decompress_d5 ✅ 3s 3s +0%
mlk_poly_getnoise_eta1_4x_native ✅ 3s 5s -40%
mlk_poly_getnoise_eta2 ✅ 3s 3s +0%
mlk_poly_mulcache_compute_c ✅ 3s 1s +200%
mlk_poly_ntt_c ✅ 3s 3s +0%
mlk_poly_reduce ✅ 3s 2s +50%
mlk_poly_reduce_c ✅ 3s 3s +0%
mlk_poly_tobytes_native ✅ 3s 2s +50%
mlk_poly_tomsg ✅ 3s 2s +50%
mlk_polyvec_basemul_acc_montgomery_cached ✅ 3s 2s +50%
mlk_polyvec_tobytes ✅ 3s 3s +0%
mlk_scalar_compress_d10 ✅ 3s 4s -25%
mlk_scalar_compress_d4 ✅ 3s 2s +50%
mlk_scalar_decompress_d11 ✅ 3s 1s +200%
mlk_scalar_decompress_d4 ✅ 3s 4s -25%
mlk_scalar_decompress_d5 ✅ 3s 3s +0%
mlk_sha3_256 ✅ 3s 2s +50%
mlk_shake128x4_absorb_once ✅ 3s 1s +200%
mlk_value_barrier_u8 ✅ 3s 2s +50%
ntt_native_aarch64 ✅ 3s 2s +50%
poly_compress_d4_native_x86_64 ✅ 3s 2s +50%
poly_compress_d5_native_x86_64 ✅ 3s 3s +0%
poly_decompress_d5_native_x86_64 ✅ 3s 3s +0%
poly_frombytes_native_x86_64 ✅ 3s 6s -50%
poly_getnoise_eta1122_4x_native ✅ 3s 3s +0%
poly_reduce_native_aarch64 ✅ 3s 1s +200%
poly_tobytes_native_x86_64 ✅ 3s 3s +0%
polyvec_basemul_acc_montgomery_cached_k3_native_x86_64 ✅ 3s 3s +0%
polyvec_basemul_acc_montgomery_cached_k4_native_aarch64 ✅ 3s 2s +50%
rej_uniform_native ✅ 3s 1s +200%
intt_native_aarch64 ✅ 2s 1s +100%
keccak_f1600_x1_native_aarch64_v84a ✅ 2s 1s +100%
keccak_f1600_x4_native_aarch64_v84a ✅ 2s 1s +100%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid ✅ 2s 2s +0%
keccak_f1600_x4_native_avx2 ✅ 2s 1s +100%
kem_enc ✅ 2s 3s -33%
kem_keypair ✅ 2s 3s -33%
mlk_ct_cmask_neg_i16 ✅ 2s 3s -33%
mlk_ct_cmov_zero ✅ 2s 2s +0%
mlk_ct_get_optblocker_i32 ✅ 2s 2s +0%
mlk_ct_get_optblocker_u8 ✅ 2s 2s +0%
mlk_keccakf1600_extract_bytes ✅ 2s 3s -33%
mlk_keccakf1600_extract_bytes (big endian) ✅ 2s 2s +0%
mlk_keccakf1600x4_extract_bytes_c ✅ 2s 3s -33%
mlk_keccakf1600x4_permute ✅ 2s 2s +0%
mlk_keccakf1600x4_xor_bytes ✅ 2s 2s +0%
mlk_keccakf1600x4_xor_bytes_c ✅ 2s 3s -33%
mlk_matvec_mul ✅ 2s 3s -33%
mlk_poly_compress_d10_native ✅ 2s 2s +0%
mlk_poly_compress_d4_c ✅ 2s 3s -33%
mlk_poly_compress_d4_native ✅ 2s 3s -33%
mlk_poly_compress_d5 ✅ 2s 3s -33%
mlk_poly_compress_d5_native ✅ 2s 2s +0%
mlk_poly_decompress_d10_c ✅ 2s 1s +100%
mlk_poly_decompress_d10_native ✅ 2s 2s +0%
mlk_poly_decompress_d4 ✅ 2s 2s +0%
mlk_poly_decompress_d5_c ✅ 2s 1s +100%
mlk_poly_decompress_dv ✅ 2s 4s -50%
mlk_poly_frombytes ✅ 2s 2s +0%
mlk_poly_getnoise_eta1122_4x ✅ 2s 4s -50%
mlk_poly_invntt_tomont_c ✅ 2s 2s +0%
mlk_poly_mulcache_compute ✅ 2s 2s +0%
mlk_poly_mulcache_compute_native ✅ 2s 3s -33%
mlk_poly_tomont ✅ 2s 1s +100%
mlk_poly_tomont_c ✅ 2s 2s +0%
mlk_polyvec_compress_du ✅ 2s 3s -33%
mlk_polyvec_decompress_du ✅ 2s 3s -33%
mlk_polyvec_mulcache_compute ✅ 2s 4s -50%
mlk_polyvec_permute_bitrev_to_custom ✅ 2s 1s +100%
mlk_polyvec_permute_bitrev_to_custom_native ✅ 2s 4s -50%
mlk_polyvec_reduce ✅ 2s 1s +100%
mlk_rej_uniform ✅ 2s 1s +100%
mlk_scalar_compress_d11 ✅ 2s 1s +100%
mlk_scalar_compress_d5 ✅ 2s 3s -33%
mlk_scalar_decompress_d10 ✅ 2s 2s +0%
mlk_scalar_signed_to_unsigned_q ✅ 2s 3s -33%
mlk_sha3_512 ✅ 2s 4s -50%
mlk_shake128x4_squeezeblocks ✅ 2s 4s -50%
mlk_shake256 ✅ 2s 1s +100%
mlk_value_barrier_i32 ✅ 2s 3s -33%
mlk_value_barrier_u32 ✅ 2s 2s +0%
ntt_native_x86_64 ✅ 2s 3s -33%
nttunpack_native_x86_64 ✅ 2s 6s -67%
poly_compress_d11_native_x86_64 ✅ 2s 3s -33%
poly_decompress_d10_native_x86_64 ✅ 2s 3s -33%
poly_invntt_tomont_native ✅ 2s 5s -60%
poly_mulcache_compute_native_aarch64 ✅ 2s 1s +100%
poly_reduce_native_x86_64 ✅ 2s 2s +0%
poly_tobytes_native_aarch64 ✅ 2s 1s +100%
poly_tomont_native_aarch64 ✅ 2s 4s -50%
polyvec_basemul_acc_montgomery_cached_k2_native_aarch64 ✅ 2s 1s +100%
polyvec_basemul_acc_montgomery_cached_k2_native_x86_64 ✅ 2s 3s -33%
polyvec_basemul_acc_montgomery_cached_k3_native_aarch64 ✅ 2s 4s -50%
sys_check_capability ✅ 2s 4s -50%
intt_native_x86_64 ✅ 1s 4s -75%
keccak_f1600_x1_native_aarch64 ✅ 1s 3s -67%
kem_keypair_derand ✅ 1s 1s +0%
mlk_barrett_reduce ✅ 1s 2s -50%
mlk_ct_memcmp ✅ 1s 3s -67%
mlk_ct_sel_uint8 ✅ 1s 2s -50%
mlk_keccakf1600_permute ✅ 1s 1s +0%
mlk_poly_compress_d11 ✅ 1s 3s -67%
mlk_poly_compress_d11_native ✅ 1s 2s -50%
mlk_poly_compress_d5_c ✅ 1s 1s +0%
mlk_poly_decompress_d11 ✅ 1s 2s -50%
mlk_poly_decompress_du ✅ 1s 1s +0%
mlk_poly_invntt_tomont ✅ 1s 1s +0%
mlk_poly_tobytes ✅ 1s 2s -50%
mlk_poly_tobytes_c ✅ 1s 2s -50%
mlk_poly_tomont_native ✅ 1s 2s -50%
mlk_polyvec_frombytes ✅ 1s 5s -80%
mlk_polyvec_invntt_tomont ✅ 1s 1s +0%
mlk_polyvec_tomont ✅ 1s 4s -75%
mlk_shake128_absorb_once ✅ 1s 3s -67%
poly_decompress_d4_native_x86_64 ✅ 1s 2s -50%

@oqs-bot

oqs-bot commented Jun 8, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-768)

Full Results (191 proofs)
Proof Status Current Previous Change
**TOTAL** ✅ 1817s 1640s +10.8%
mlk_indcpa_keypair_derand ✅ 348s 302s +15%
mlk_indcpa_enc ✅ 265s 249s +6%
mlk_poly_rej_uniform ✅ 160s 127s +26%
mlk_rej_uniform_c ✅ 142s 113s +26%
rej_uniform_native_x86_64 ✅ 62s 53s +17%
mlk_polyvec_basemul_acc_montgomery_cached_c ✅ 57s 47s +21%
poly_ntt_native ✅ 45s 38s +18%
mlk_ntt_layer ✅ 40s 29s +38%
rej_uniform_native_aarch64 ✅ 40s 35s +14%
mlk_poly_reduce_native ✅ 36s 34s +6%
mlk_keccak_squeezeblocks_x4 ✅ 24s 24s +0%
mlk_fqmul ✅ 18s 17s +6%
polyvec_basemul_acc_montgomery_cached_native ✅ 18s 14s +29%
mlk_poly_decompress_d10_native ✅ 17s 12s +42%
keccakf1600x4_permute_native_x4 ✅ 16s 18s -11%
mlk_poly_decompress_d4_native ✅ 15s 12s +25%
mlk_polyvec_add ✅ 13s 10s +30%
mlk_indcpa_dec ✅ 12s 11s +9%
mlk_poly_frombytes_native ✅ 11s 7s +57%
mlk_poly_frommsg ✅ 11s 9s +22%
mlk_keccak_squeeze_once ✅ 8s 7s +14%
mlk_keccak_squeezeblocks ✅ 8s 8s +0%
mlk_poly_rej_uniform_x4 ✅ 8s 6s +33%
mlk_ntt_butterfly_block ✅ 7s 6s +17%
mlk_poly_add ✅ 7s 4s +75%
mlk_invntt_layer ✅ 6s 4s +50%
mlk_poly_ntt ✅ 6s 7s -14%
kem_dec ✅ 5s 5s +0%
kem_enc ✅ 5s 4s +25%
mlk_keccak_absorb_once ✅ 5s 3s +67%
mlk_keccak_absorb_once_x4 ✅ 5s 7s -29%
mlk_poly_sub ✅ 5s 6s -17%
mlk_poly_tobytes_native ✅ 5s 3s +67%
mlk_scalar_decompress_d4 ✅ 5s 3s +67%
poly_compress_d10_native_x86_64 ✅ 5s 2s +150%
poly_compress_d11_native_x86_64 ✅ 5s 3s +67%
poly_decompress_d10_native_x86_64 ✅ 5s 2s +150%
poly_decompress_d4_native_x86_64 ✅ 5s 5s +0%
poly_frombytes_native_x86_64 ✅ 5s 6s -17%
kem_check_sk ✅ 4s 2s +100%
mlk_enc_getnoise_eta1_eta2 ✅ 4s 1s +300%
mlk_keccakf1600_extract_bytes ✅ 4s 3s +33%
mlk_poly_cbd_eta1 ✅ 4s 2s +100%
mlk_poly_cbd_eta2 ✅ 4s 1s +300%
mlk_poly_compress_d11_c ✅ 4s 1s +300%
mlk_poly_frombytes ✅ 4s 4s +0%
mlk_poly_frombytes_c ✅ 4s 7s -43%
mlk_poly_getnoise_eta1_4x ✅ 4s 1s +300%
mlk_poly_mulcache_compute_c ✅ 4s 2s +100%
mlk_scalar_compress_d11 ✅ 4s 5s -20%
mlk_scalar_signed_to_unsigned_q ✅ 4s 3s +33%
ntt_native_aarch64 ✅ 4s 3s +33%
poly_reduce_native_x86_64 ✅ 4s 2s +100%
sys_check_capability ✅ 4s 2s +100%
intt_native_aarch64 ✅ 3s 2s +50%
keccak_f1600_x1_native_aarch64_v84a ✅ 3s 1s +200%
keccak_f1600_x4_native_avx2 ✅ 3s 1s +200%
keccakf1600x4_xor_bytes_native ✅ 3s 2s +50%
kem_keypair_derand ✅ 3s 3s +0%
mlk_ct_cmask_nonzero_u16 ✅ 3s 2s +50%
mlk_ct_cmask_nonzero_u8 ✅ 3s 1s +200%
mlk_ct_get_optblocker_u8 ✅ 3s 2s +50%
mlk_ct_memcmp ✅ 3s 3s +0%
mlk_gen_matrix_serial ✅ 3s 4s -25%
mlk_keccakf1600_extract_bytes (big endian) ✅ 3s 2s +50%
mlk_keccakf1600_permute_c ✅ 3s 5s -40%
mlk_keccakf1600x4_xor_bytes ✅ 3s 2s +50%
mlk_matvec_mul ✅ 3s 4s -25%
mlk_poly_compress_d11 ✅ 3s 2s +50%
mlk_poly_compress_d11_native ✅ 3s 3s +0%
mlk_poly_compress_d4_c ✅ 3s 3s +0%
mlk_poly_compress_d5_c ✅ 3s 2s +50%
mlk_poly_decompress_d10 ✅ 3s 2s +50%
mlk_poly_decompress_d10_c ✅ 3s 3s +0%
mlk_poly_decompress_d4_c ✅ 3s 5s -40%
mlk_poly_decompress_dv ✅ 3s 3s +0%
mlk_poly_invntt_tomont_c ✅ 3s 1s +200%
mlk_poly_reduce_c ✅ 3s 3s +0%
mlk_poly_tomont_native ✅ 3s 2s +50%
mlk_polyvec_compress_du ✅ 3s 4s -25%
mlk_polyvec_decompress_du ✅ 3s 2s +50%
mlk_polyvec_frombytes ✅ 3s 3s +0%
mlk_polyvec_invntt_tomont ✅ 3s 3s +0%
mlk_polyvec_permute_bitrev_to_custom ✅ 3s 2s +50%
mlk_polyvec_permute_bitrev_to_custom_native ✅ 3s 2s +50%
mlk_polyvec_reduce ✅ 3s 1s +200%
mlk_polyvec_tomont ✅ 3s 1s +200%
mlk_scalar_compress_d4 ✅ 3s 3s +0%
mlk_scalar_compress_d5 ✅ 3s 5s -40%
mlk_sha3_512 ✅ 3s 4s -25%
mlk_shake128_squeezeblocks ✅ 3s 2s +50%
mlk_shake128x4_squeezeblocks ✅ 3s 1s +200%
mlk_shake256x4 ✅ 3s 5s -40%
mlk_value_barrier_u32 ✅ 3s 2s +50%
poly_compress_d4_native_x86_64 ✅ 3s 2s +50%
poly_invntt_tomont_native ✅ 3s 4s -25%
poly_tomont_native_aarch64 ✅ 3s 5s -40%
polyvec_basemul_acc_montgomery_cached_k2_native_aarch64 ✅ 3s 2s +50%
polyvec_basemul_acc_montgomery_cached_k2_native_x86_64 ✅ 3s 4s -25%
polyvec_basemul_acc_montgomery_cached_k3_native_aarch64 ✅ 3s 2s +50%
polyvec_basemul_acc_montgomery_cached_k4_native_x86_64 ✅ 3s 3s +0%
rej_uniform_native ✅ 3s 4s -25%
intt_native_x86_64 ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v84a ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid ✅ 2s 2s +0%
kem_check_pk ✅ 2s 3s -33%
kem_enc_derand ✅ 2s 3s -33%
kem_keypair ✅ 2s 2s +0%
mlk_barrett_reduce ✅ 2s 1s +100%
mlk_check_pct ✅ 2s 2s +0%
mlk_ct_cmask_neg_i16 ✅ 2s 2s +0%
mlk_ct_cmov_zero ✅ 2s 2s +0%
mlk_ct_get_optblocker_u32 ✅ 2s 4s -50%
mlk_ct_sel_uint8 ✅ 2s 2s +0%
mlk_gen_matrix ✅ 2s 3s -33%
mlk_keccakf1600_permute ✅ 2s 2s +0%
mlk_keccakf1600_xor_bytes ✅ 2s 3s -33%
mlk_keccakf1600_xor_bytes (big endian) ✅ 2s 6s -67%
mlk_keccakf1600x4_extract_bytes ✅ 2s 3s -33%
mlk_keccakf1600x4_permute ✅ 2s 1s +100%
mlk_keccakf1600x4_xor_bytes_c ✅ 2s 2s +0%
mlk_keypair_getnoise_eta1 ✅ 2s 2s +0%
mlk_montgomery_reduce ✅ 2s 2s +0%
mlk_poly_compress_d10 ✅ 2s 2s +0%
mlk_poly_compress_d10_native ✅ 2s 2s +0%
mlk_poly_compress_d5 ✅ 2s 2s +0%
mlk_poly_compress_d5_native ✅ 2s 3s -33%
mlk_poly_compress_dv ✅ 2s 4s -50%
mlk_poly_decompress_d11_native ✅ 2s 1s +100%
mlk_poly_decompress_d4 ✅ 2s 2s +0%
mlk_poly_decompress_d5_c ✅ 2s 2s +0%
mlk_poly_decompress_d5_native ✅ 2s 3s -33%
mlk_poly_decompress_du ✅ 2s 3s -33%
mlk_poly_getnoise_eta1122_4x ✅ 2s 1s +100%
mlk_poly_getnoise_eta1_4x_native ✅ 2s 3s -33%
mlk_poly_invntt_tomont ✅ 2s 2s +0%
mlk_poly_mulcache_compute ✅ 2s 3s -33%
mlk_poly_mulcache_compute_native ✅ 2s 1s +100%
mlk_poly_ntt_c ✅ 2s 3s -33%
mlk_poly_reduce ✅ 2s 3s -33%
mlk_poly_tobytes_c ✅ 2s 2s +0%
mlk_poly_tomont_c ✅ 2s 2s +0%
mlk_polymat_permute_bitrev_to_custom ✅ 2s 3s -33%
mlk_polyvec_basemul_acc_montgomery_cached ✅ 2s 2s +0%
mlk_polyvec_ntt ✅ 2s 6s -67%
mlk_polyvec_tobytes ✅ 2s 4s -50%
mlk_scalar_compress_d1 ✅ 2s 2s +0%
mlk_scalar_compress_d10 ✅ 2s 2s +0%
mlk_scalar_decompress_d10 ✅ 2s 2s +0%
mlk_scalar_decompress_d11 ✅ 2s 2s +0%
mlk_sha3_256 ✅ 2s 3s -33%
mlk_shake128_absorb_once ✅ 2s 2s +0%
mlk_shake128x4_absorb_once ✅ 2s 4s -50%
mlk_value_barrier_i32 ✅ 2s 3s -33%
mlk_value_barrier_u8 ✅ 2s 3s -33%
ntt_native_x86_64 ✅ 2s 1s +100%
nttunpack_native_x86_64 ✅ 2s 2s +0%
poly_compress_d5_native_x86_64 ✅ 2s 2s +0%
poly_decompress_d11_native_x86_64 ✅ 2s 2s +0%
poly_decompress_d5_native_x86_64 ✅ 2s 2s +0%
poly_mulcache_compute_native_aarch64 ✅ 2s 3s -33%
poly_mulcache_compute_native_x86_64 ✅ 2s 2s +0%
poly_reduce_native_aarch64 ✅ 2s 4s -50%
poly_tobytes_native_x86_64 ✅ 2s 3s -33%
poly_tomont_native_x86_64 ✅ 2s 4s -50%
keccak_f1600_x1_native_aarch64 ✅ 1s 1s +0%
keccakf1600_permute_native ✅ 1s 1s +0%
keccakf1600x4_extract_bytes_native ✅ 1s 5s -80%
mlk_ct_get_optblocker_i32 ✅ 1s 2s -50%
mlk_ct_sel_int16 ✅ 1s 3s -67%
mlk_keccakf1600x4_extract_bytes_c ✅ 1s 1s +0%
mlk_poly_compress_d10_c ✅ 1s 2s -50%
mlk_poly_compress_d4 ✅ 1s 1s +0%
mlk_poly_compress_d4_native ✅ 1s 2s -50%
mlk_poly_compress_du ✅ 1s 3s -67%
mlk_poly_decompress_d11 ✅ 1s 5s -80%
mlk_poly_decompress_d11_c ✅ 1s 1s +0%
mlk_poly_decompress_d5 ✅ 1s 2s -50%
mlk_poly_getnoise_eta2 ✅ 1s 3s -67%
mlk_poly_tobytes ✅ 1s 2s -50%
mlk_poly_tomont ✅ 1s 7s -86%
mlk_poly_tomsg ✅ 1s 4s -75%
mlk_polyvec_mulcache_compute ✅ 1s 2s -50%
mlk_rej_uniform ✅ 1s 4s -75%
mlk_scalar_decompress_d5 ✅ 1s 3s -67%
mlk_shake256 ✅ 1s 2s -50%
poly_getnoise_eta1122_4x_native ✅ 1s 1s +0%
poly_tobytes_native_aarch64 ✅ 1s 1s +0%
polyvec_basemul_acc_montgomery_cached_k3_native_x86_64 ✅ 1s 1s +0%
polyvec_basemul_acc_montgomery_cached_k4_native_aarch64 ✅ 1s 1s +0%

@willieyz willieyz force-pushed the win-sup-rng-fail branch from 7cd4bfa to 6bba531 Compare June 9, 2026 08:01
@willieyz willieyz marked this pull request as ready for review June 9, 2026 15:29
@willieyz willieyz requested a review from a team as a code owner June 9, 2026 15:29
@willieyz willieyz requested a review from mkannwischer June 9, 2026 15:29
@willieyz willieyz force-pushed the win-sup-rng-fail branch 3 times, most recently from e66e8b4 to 05c7d8e Compare June 15, 2026 17:34
@willieyz willieyz mentioned this pull request Jun 15, 2026
Closed
mkannwischer
mkannwischer requested changes Jun 16, 2026
View reviewed changes

@mkannwischer mkannwischer left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@willieyz, thanks!
It's not true that we don't have tests on Windows. We do have tests on Windows using Mingw-w64. Can you adjust the commit message to reflect the gap you are closing (Tests on Windows using MSVC).

mkannwischer
mkannwischer requested changes Jun 16, 2026
View reviewed changes

@mkannwischer mkannwischer left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Also can we please close the remaining gap in a single PR, i.e, rng_fail, unit, alloc, wycheproof - that should all be straightforward?

@willieyz willieyz changed the title Add rng_fail test Windows support (C backend only) Add rng_fail test, alloc test support for MSVC-based tests on Windows Jun 16, 2026
@willieyz willieyz changed the title Add rng_fail test, alloc test support for MSVC-based tests on Windows Add Windows MSVC test support: rng_fail, alloc, wycheproof, unit, (C backend only) Jun 16, 2026
@willieyz willieyz marked this pull request as draft June 16, 2026 17:06
@willieyz

willieyz commented Jun 16, 2026

Copy link
Copy Markdown
Contributor Author

@willieyz, thanks! It's not true that we don't have tests on Windows. We do have tests on Windows using Mingw-w64. Can you adjust the commit message to reflect the gap you are closing (Tests on Windows using MSVC).

Hello @mkannwischer,

Thank you for the review!
I've updated the commit message accordingly. Following your comment, I'll also address the remaining gaps in this PR. I've converted the PR back to draft status for now, and I will mark it as ready for review again once all the missing tests have been added.

Thanks again for taking the time to review and for the feedback.

@willieyz willieyz changed the title Add Windows MSVC test support: rng_fail, alloc, wycheproof, unit, (C backend only) Add Windows MSVC test support: rng_fail, alloc, wycheproof Jun 18, 2026
@willieyz willieyz marked this pull request as ready for review June 18, 2026 04:57
willieyz added 3 commits June 22, 2026 16:33
@willieyz
Add rng_fail test support for Windows MSVC
ac3b42f 
mlkem-native already runs tests on Windows via Mingw-w64, but the
MSVC/nmake build has no rng_fail test coverage. This commit adds the
link rules to Makefile.Microsoft_nmake to enable rng_fail tests against
the portable C backend under MSVC.

Signed-off-by: willieyz <willie.zhao@chelpis.com>
@willieyz
Add alloc test support for Windows MSVC
7ce2b43 
mlkem-native already runs tests on Windows via Mingw-w64, but the
MSVC/nmake build has no alloc test coverage. This commit adds the
compile and link rules to Makefile.Microsoft_nmake to enable alloc
tests against the portable C backend under MSVC.

Signed-off-by: willieyz <willie.zhao@chelpis.com>
@willieyz
Add wycheproof test support for Windows MSVC
4b21918 
mlkem-native already runs tests on Windows via Mingw-w64, but the
MSVC/nmake build has no wycheproof test coverage.
This commit adds the compile and link rules to
Makefile.Microsoft_nmake, also add the run_wycheproof target, to enable
wycheproof tests against the portable C backend under MSVC.

Signed-off-by: willieyz <willie.zhao@chelpis.com>
@willieyz willieyz requested a review from mkannwischer June 22, 2026 16:34
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@mkannwischer mkannwischer Awaiting requested review from mkannwischer

Requested changes must be addressed to merge this pull request.

Assignees

No one assigned

Labels

needs-mldsa-native-port

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@willieyz @oqs-bot @mkannwischer